es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id} , p,
q:({e:E| loc(e) = loc(e1)  Id} {e:E| loc(e) = loc(e1)  Id} ).
e1 loc e2   q(e1,e2)  [e1;e2]~([a,b].p(a,b))*[a,b].q(a,b) 

latex

Definitions	x:A. B(x), , P  Q, x(s1,s2), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x:A. B(x), t  T, , P & Q, {i..j}, A c B, i  j < k, A  B, A, False
Lemmas	es-loc wf, Id wf, es-le wf, es-E wf, event system wf, int seg wf, le wf, es-locl wf, es-pred wf